$\exists$${\it code}$:($\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$). Surj($\mathbb{N}$; $\mathbb{N}\times\mathbb{N}$; ${\it code}$)